Nuprl Lemma : fpf-rename_wf 11,40
A, C:Type, B:(AType), D:(CType), eq:EqDecider(C), r:(AC), f:a:A fp B(a).
(a:A. D(r(a)) = B(a))  (rename(r;f)  c:C fp D(c)) 
latex

DefinitionsP  Q, P  Q, A c B, eqof(d), x:A. B(x), P & Q, b, P  Q, , x. t(x), EqDecider(T), a:A fp B(a), rename(r;f), map(f;as), x(s), (x  l), x:A. B(x), hd(l), t  T
Lemmasl member wf, map wf, deq wf, fpf wf, eqof wf, hd-filter, assert wf, member map, deq property

origin